COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	goedel[f81,jmc]		Kreisel's essence of Goedel's theorem and applications
C00005 ENDMK
C⊗;
goedel[f81,jmc]		Kreisel's essence of Goedel's theorem and applications

From Kreisel's Goedel obituary

	"Let  S  be a class of (formulas defining) number-theoretic
predicates with one and two arguments, closed under identification of
variables and negation; thus if  F(n,m)  is in  S, so is  ¬F(n,n).
Then there is no (binary) predicate in  S  which enumerates all
(monadic) predicates in  S.  This means, as usual, that no formula
F(n,m)  in  S  has the property:

	[for each formula  G(m) of  S  there is a number  g'  such that

	∀m[F(g',m) ≡ G(m)].

a counter example is obtained by taking  ¬F(m,m)  for  G(m), and putting
  m = g'."

The above is the essence of the proof of Goedel's first incompleteness
theorem.

	Perhaps, it can be used to prove the undecidability of totality of LISP
functions as follows: (i) In the above, replace "number-theoretic" by
"LISP-theoretic".  (ii) Let  S  be the class of all total LISP functions
of one and two arguments.  (iii) The  F(n,m) shown not to exist would
enumerate all total one argument LISP predicates.  Hmm, this isn't
obviously what we want.  Oh yes, it gives us what we want.  Suppose we
had a total LISP function  total(e)  that determined whether a LISP
function were total.  Then the function   F(n,m)  defined by

	F(n,m) ← if total(n) then eval(<n,<quote,m>>,nil) else ATOM

would enumerate all total LISP predicates in Kreisel's sense.

	This proves there is no test for totality.  A bit more must
be said to show that termination is undecidable in the individual
case.  Suppose the predicate 

	terminates(fn,arg),

which is true iff the application of the function  fn  to the list
args  of arguments terminates, were a LISP function.  Then

	P(n,m) = if terminates(n,m) then eval(<n,<quote,m>>,nil) else nil

	¬P(n,n) = if terminates(n,n) then ¬eval(<,<quote,n>>,nil) else true

		= P(a,n)